$\forall$$T$:Type, $R$, ${\it R'}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$). ($R$ $\Lleftarrow\!\Rrightarrow$\{$T$\} ${\it R'}$) $\Rightarrow$ ($R$ $\equiv>$\{$T$\} ${\it R'}$)